<?xml version="1.0" encoding="UTF-8"?>

<!--

Example of equational factorial function definition

-->

<!DOCTYPE Document [
  <!ENTITY rif  "http://www.w3.org/2007/rif#">
  <!ENTITY pred "http://www.w3.org/2007/rif-builtin-predicate#">
  <!ENTITY func "http://www.w3.org/2007/rif-builtin-function#">
  <!ENTITY xs   "http://www.w3.org/2001/XMLSchema#">
]>
  
<Document 
    xmlns="http://www.w3.org/2007/rif#"
    xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
    xmlns:xs="http://www.w3.org/2001/XMLSchema#">
  <payload>
   <Group>
    <sentence>
     <Equal>
       <left>
         <Expr>
           <op><Const type="&rif;local">factorial</Const></op>
           <args ordered="yes"><Const type="&xs;integer">0</Const></args>
         </Expr>
       </left>
       <right><Const type="&xs;integer">1</Const></right>
     </Equal>
    </sentence>
    <sentence>
     <Forall>
       <declare><Var>N</Var></declare>
       <formula>
         <Implies>
           <if>
             <Atom>
               <op><Const type="&rif;iri">&pred;numeric-greater-than</Const></op>
               <args ordered="yes">
                 <Var>N</Var>
                 <Const type="&xs;integer">0</Const>
               </args>
             </Atom>
           </if>
           <then>
             <Equal>
               <left>
                 <Expr>
                   <op><Const type="&rif;local">factorial</Const></op>
                   <args ordered="yes"><Var>N</Var></args>
                 </Expr>
               </left>
               <right>
                  <Expr>
                     <op><Const type="&rif;iri">&func;numeric-multiply</Const></op>
                     <args ordered="yes">
                       <Var>N</Var>
                       <Expr>
                         <op><Const type="&rif;local">factorial</Const></op>
                         <args ordered="yes">
                           <Expr>
                             <op><Const type="&rif;iri">&func;numeric-subtract</Const></op>
                             <args ordered="yes">
                               <Var>N</Var>
                               <Const type="&xs;integer">1</Const>
                             </args>
                           </Expr>
                         </args>
                       </Expr>
                     </args>
                  </Expr>
               </right>
             </Equal>
           </then>
         </Implies>
       </formula>
     </Forall>
    </sentence>
   </Group>
  </payload>
 </Document>
